Nuprl Lemma : assert_of_mon_eq
13,42
postcript
pdf
s
:Mon,
a
,
b
:|
s
|. (
(
a
=
b
))
(
a
=
b
)
latex
Up
groups
1
Definitions of Statement
Mon
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
Mon
,
P
&
Q
,
IsEqFun(
T
;
eq
)
Lemmas
mon
wf
,
grp
car
wf
,
mon
properties
origin
s:Mon, a, b:|s|. (
(a =
b)) 
(a = b) s:Mon, a, b:|s|. ((a = b)) (a = b) 
Tx:A. B(x)